f, g:x:Knd fp Type, x:Knd. x  dom(f  g)  x  dom(f)  x  dom(g) 

latex

Definitions	a:A fp B(a), x:A. B(x), x. t(x), t  T, Knd, f  g, P  Q, P & Q, P  Q, P  Q, P  Q, Prop, b, x  dom(f), KindDeq, Top
Lemmas	fpf-trivial-subtype-top, Kind-deq wf, fpf-dom wf, assert wf, top wf, fpf-join wf, fpf-join-dom, iff functionality wrt iff, Knd wf, fpf wf